形式化验证的阿喀琉斯之踵
（原文最早于2018年4月发表在老石的个人博客”老石谈芯“，可点击文末的“阅读全文”查看）
目 录
战神的脚踝：形式化验证的主要问题
如何使用形式化验证
形式化验证流程
老石眼中的现代验证方法学
战神的脚踝：
形式化验证的主要问题
相比于传统的基于仿真的验证方法学，形式化验证有着似乎无可比拟的优势，看起来几乎是完美的验证方法学。可惜的是，形式化验证有着非常显著的缺点，其中最主要的就是所谓的“状态爆炸”问题（state explosion）。
顾名思义，这代表了在某个设计中，理论上存在的状态可能非常多，超出了形式化验证工具可以处理的范围。
例如，在一个简单的N位计数器中，可能存在2的N次方个状态，且状态数量随着计数器位数的增加呈指数级增长。同样的状态爆炸问题存在于存储器、各类数学运算单元如乘法器等等，如下图示意的是M1xM2结果的状态与M1和M2的状态数呈指数级关系。
状态爆炸问题是由形式化验证——具体而言是形式化验证中最为常用的模型验证（Model Checking）——的工作机制决定的，是形式化验证的根本性问题，无法通过优化算法或者工具完全解决。
但是，值得欣慰的是，学术界和业界也在不断探索用来缓解状态爆炸问题的各种方法。在理论上，有学者提出了以下方法，如：
符号模型验证（Symbolic Model Checking），即使用二元决策图（Binary Decision Diagrams – BDD）而非独立的状态列表来表达状态空间；
偏序约减（Partial Order Reduction），即检查各个状态和行为间的独立性以减小整体的状态空间；
基于反例的抽象优化（Counterexample-Guided Abstraction Refinement），即自适应的寻找合适的抽象层次，实现精度和运行时间的折中。
有界模型验证（Bounded Model Checking），即使用SAT（Boolean satisfiability）求解器在一定边界条件下寻找反例。
在实际应用中，业界也有一系列应对状态爆炸问题的方法，我将在下一章进行详细阐述。
2
如何使用形式化验证
那么，应该如何着手使用形式化验证？首先需要考虑如何将设计规约和需求用形式化的方法表述出来。
验证的本质就是将设计与设计规约进行一一比对的过程。在电路仿真中，通常使用参考模型（reference model）作为设计规约的实现形式。
参考模型通常由高级语言，如C/C++、SystemC、MATLAB等实现，但有时也会通过RTL语言如SystemVerilog实现。与此不同的是，在形式化验证方法中，设计规约是通过形式化的语言进行抽象和描述的，而并不需要参考模型。
设计规约通常会被拆分成若干条“属性”（Property），然后通过SystemVerilog断言（SystemVerilog Assertion – SVA）来进行描述。
SVA是SystemVerilog语言的一个子集，其实它已然被广泛用于传统的电路仿真中，但使用范围比较受限，主要用来检查在仿真中某些状态（通常为异常状态）是否会发生。在形式化验证中，SVA则是作为主要的编程语言，用来描述设计规约的各条属性、对设计的行为进行建模、提供实际的约束、提取覆盖率等等。
SVA的层次可以根据所表达的复杂度分为如下四级：
1. 布尔运算（Booleans），如
2. 序列（sequence），用来表达在一段时间内发生的一系列布尔运算。因此可见序列的表示需要一个明确的时钟作为参考。例如：
这代表当req置一后再过两个时钟周期，grant再置一。
3. 属性（property），用来组合多个序列，并以此表明在设计中需要满足的某种逻辑关系。如：
其中A和B都为序列。本例中前者代表当A成立时，B在同一个周期内也必须成立；后者代表当A成立时，B在下一个周期必须成立。
4. 断言声明（assertion statements），用来表示对一则SVA属性所进行的动作，例如：
这代表将对括号内的property进行断言检查。
断言声明通常使用以下三个关键词之一：assert，assume和cover。这三个关键词在形式化验证环境中的语义和在电路仿真中有所不同：
Assert：表示给定的断言声明（statement）必须在任何条件下都满足；
Assume：用来指定各种形式化验证的约束条件；
Cover：用来表明在形式化验证的过程中必须要覆盖到的情况。
3
形式化验证流程
由于篇幅所限，其他更深入的有关SVA的介绍和举例无法在本文给出。本文想强调的是，在形式化验证中，各种设计规约、约束条件、验证目标、覆盖点等，都是通过SVA进行表述和建模的。
这样，可以把形式化验证流程图扩展为如下图所示：
可以看到，形式化验证引擎的输入输出都进行了一些扩展。在输入端，除了在仿真中也需要的待测模块以外，形式化验证还需要对输入进行一定的约束，并通过SVA的描述，提供待验证的断言和覆盖点。
通常来讲，使用形式化验证的第一步，并非是立即编写各种断言，而是构思需要对整个设计和验证环境添加怎样的约束。
形式化约束的意义在于能很大程度上的减小状态空间，一方面能引导形式化验证工具在更加合理的状态区间中进行更有效的断言判定，另一方面能够从一开始就杜绝一些不合理的状态或条件的出现，从而避免验证出现漏报（false negative）。为形式化验证添加约束还能“强迫”设计者和验证工程师在整体上全面思考设计规约以及设计需求，从而在早期发现设计规约和需求中的漏洞和不足。
在明确各种约束条件之后，接下来需要考虑设计中存在哪些目标状态，并通过覆盖点进行覆盖。这与使用随机约束的验证方法中，提取功能覆盖率的思想比较类似。通常这些目标状态都在验证计划中给出。
需要注意的是，在形式化验证中，覆盖点还有一个重要作用是防止误报（false positive）的出现。最极端的例子是，如果不给出任何断言，那么形式化验证工具就会给出全部断言都被证明的误报。因此需要覆盖点对目标状态进行覆盖，确保工具对相关断言的确进行了证明。
在形式化验证工具的输出端，通常会给出三类信息：
若断言得到证明，则会给出已经被证明的断言列表；
若断言被证明有误，则会给出一个反例，如上文所述通常为最小实例；
若在有限时间之内，工具无法给出证明或反证，则会标明该断言的证明没有定论（inconclusive）。
有很多种可能性会导致出现最后一种情况，例如证明时间太短、断言及属性过于复杂等，但通常代表此时的状态空间太大，已经超出了形式化工具可以证明的范围。
此时，应该考虑着手减小状态空间，例如考虑简化断言、提供更多约束、尝试其他的形式化验证引擎等。也可以使用更进一步形式化验证技巧，如使用抽象模型（abstraction），设置黑盒（blackbox）或断点（cut-point），对待测设计采用分而治之的策略等。
再比如，对于一个大小为32位宽、512个存储单元的存储器，理论上它的状态空间存在2^(32*512)个状态， 即大约十亿的一千次方，已经远超计算机可以计算的范围。
其实，对于存储器本身而言，它通常作为一个可配置的IP使用，对于使用存储器IP的设计，验证存储器自身的功能并非验证的目的。而且，我们往往可以安全的假设，存储器本身已经经过了IP提供商的完整验证，可以直接使用。此外，可以注意到每个存储器的存储单元均相互独立，很多情况下两个存储单元的内容并不会相互影响。
在这种情况下，我们可以使用针对存储器的抽象模型，只对少数存储单元进行精确建模，而不需关心其他单元，那么可以将整体的状态空间下降为2^(32*3)个状态。
对形式化验证中的抽象模型的研究一直是业界和学界的热点之一，比如，英国Imagination公司的Arshish Darbari等人曾经发表过多篇文章，详细阐述了关于FIFO、Arbiter等模块的形式化抽象方法。我的博士导师，伦敦帝国理工学院的Constantinides教授也曾对多项式数据通路的形式化验证开展过一系列理论研究工作。形式化验证咨询机构Oski也发表过一系列文章，详细讲解了诸如如何对FIFO等底层模块进行形式化抽象，如下图所示。
同时，形式化验证工具的提供商，如Candence和Synopsys也都提供了一些常用模块，如FIFO、存储器、乘法器等的抽象模型。
综上所述，一个较为完整的形式化验证环境会如下图所示。
4
老石眼中的现代验证方法学
在笔者眼中，形式化验证将在现代验证方法学中慢慢占有越来越重要的地位。这主要是由于形式化验证独特的工作原理，及其先天优于基于电路仿真的验证方法的各类特性。
同时，形式化验证适用于多种不同的模块层级，从小规模的IP设计，到大规模的系统集成，都有可能使用形式化的方法进行验证。很多业界的公司都早已开展形式化验证的使用，比如英特尔就对其i7处理器的某核心部件全部使用形式化方法进行验证。
随着EDA工具的不断完善，普通的工程师使用者并不需要掌握任何形式化理论或数学模型推导，这些过程都已被封装在工具中，这样大大简化了形式化验证的使用门槛。
形式化验证另一个主要的作用在于，能够帮助设计者充分严谨的思考设计需求和规约，并在设计早期就能有效发现各类漏洞，而无需等待复杂的测试平台搭建完成。
不过需要记住的是，形式化验证也伴随着先天的缺点，即不能有效处理拥有大量状态的设计，如存储器、数学运算器等。为了应对这样的情况，验证工程师需要掌握一些形式化验证技巧和抽象方法。
此外，形式化验证与电路仿真的思考角度完全不同，一个熟练使用UVM和随机约束的验证工程师不一定能在短时间内很好的掌握形式化验证的思想和工作方法。这几点都使得形式化验证又不是那么简单易用。
因此，业界的共识在于，充分利用形式化验证和电路仿真的优点，扬长避短，在一个完整的项目周期内协同使用不同的验证方法学。业界有关项目进行时间和漏洞数量关系、修复漏洞的花费三者关系的经验图如下所示，可见在项目开发初期，是各类漏洞存在的高发期，但此时修复漏洞所需要的成本最少。等到项目行将结束并流片的时候，漏洞很难被找到，但一旦出现就往往需要花费大量成本进行修复。
因此，在项目早期，可以利用形式化方法逐步完善设计规约，同时发现各类早期的问题和简单的漏洞。设计者也可以负责编写各类断言，而验证工程师负责形式化平台的搭建，以及更复杂断言的设计。
与此同时，使用UVM等方法学搭建电路仿真平台，用以在更高层次（如系统集成时）、和项目中后期通过不间断的回归测试发现设计漏洞。当基本测试完成后，可以使用硬件模拟和FPGA原型设计等方法，再进行大量实际数据的测试。特别是对基于FPGA系统的设计，由于FPGA的可编程性，有条件的话可以更早进行硬件测试。
综上，在老石看来，现代的验证方法学应该是形式化验证、电路仿真、硬件测试的三位一体的集合和统一。我也期待形式化验证方法能在业界受到更加广泛的使用。
最后，推荐一本介绍形式化验证方法学的书：《Formal Verification: An Essential Toolkit For Modern VLSI Design》，由我的同事Eric Seligman等编写。Eric是英特尔在形式化验证领域的大牛，非常平易近人，对技术的传授和讨论不遗余力且毫无保留。这本应该是目前市面上最好的有关形式化验证的书籍，我通读过，获益匪浅。只可惜国内目前好像还没有引进，我正在和出版社积极联系，希望这本书的中文版能早日和国内的读者朋友们见面。